Nuprl Lemma : compose_wf_for_mon_hom
13,42
postcript
pdf
A
,
B
,
C
:IMonoid,
f
:MonHom(
A
,
B
),
g
:MonHom(
B
,
C
). (
g
o
f
)
MonHom(
A
,
C
)
latex
Up
groups
1
Definitions of Statement
IMonoid
,
IsMonHom{
M1
,
M2
}(
f
)
,
MonHom(
M1
,
M2
)
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
MonHom(
M1
,
M2
)
,
FunThru2op(
A
;
B
;
opa
;
opb
;
f
)
,
P
&
Q
,
IsMonHom{
M1
,
M2
}(
f
)
,
P
Q
,
P
Q
,
P
Q
,
f
o
g
,
x
f
y
,
IMonoid
,
Lemmas
imon
wf
,
monoid
hom
wf
,
monoid
hom
p
wf
,
grp
car
wf
,
compose
wf
,
monoid
hom
properties
,
grp
op
wf
origin
A, B, C:IMonoid, f:MonHom(A,B), g:MonHom(B,C). (g o f) 
MonHom(A,C) A, B, C:IMonoid, f:MonHom(A,B), g:MonHom(B,C). (g o f) MonHom(A,C) Tx:A. B(x)
Q
Q Q